test(mbt): Add Model Based Test for Emerald by erickpintor · Pull Request #201 · informalsystems/emerald

erickpintor · 2026-01-29T13:26:29Z

This patch connects the newly added Quint specs to Emerald's code via the Quint Connect library.

PS: the best files to start reviewing are probable tests.rs and driver.rs.

erickpintor · 2026-01-29T22:03:20Z

tests/mbt/src/tests.rs

+#[quint_run(
+    spec = "../../specs/emerald_mbt.qnt",
+    step = "step_no_failures",
+    max_samples = 32,
+    max_steps = 128
+)]
+fn simulation_no_failures() -> impl Driver {
+    EmeraldDriver::default()
+}
+
+#[quint_run(
+    spec = "../../specs/emerald_mbt.qnt",
+    step = "step_with_failures",
+    max_samples = 32,
+    max_steps = 128
+)]
+fn simulation_with_failures() -> impl Driver {
+    EmeraldDriver::default()
+}


First uncached run took about 30m in the CI. Let me know if you want to generate fewer traces or reduce the number of steps to minimize test time.

bugarela

All good from my side!

This patch connects the newly added Quint specs to Emerald's code via the Quint Connect library.

rnbguy · 2026-02-05T16:57:12Z

tests/mbt/src/reth.rs

+    let res = Command::new("make")
+        .env("RETH_NODES", nodes)
+        .arg(cmd)
+        .current_dir("../..")


can we use absolute path here?

you may use CARGO_MANIFEST_DIR.

rnbguy · 2026-02-05T16:57:42Z

tests/mbt/src/reth.rs

+    if !res.status.success() {
+        bail!(
+            "Failed to run make command: {}",
+            String::from_utf8_lossy(&res.stderr)
+        );
+    }


you can use anyhow::ensure()

rnbguy · 2026-02-05T16:58:28Z

tests/mbt/src/runtime.rs

+impl Runtime {
+    pub fn new(temp_dir: TempDir) -> Result<Self> {
+        Ok(Self {
+            tokio: tokio::runtime::Runtime::new()?,


why not TokioRt::new() ?

rnbguy · 2026-02-05T17:00:16Z

.github/workflows/test.yml

+      - name: Run Forge build
+        run: forge build
+        if: steps.filter.outputs.code == 'true'


make mbt-test is already calling forge build.

rnbguy · 2026-02-05T17:04:11Z

tests/mbt/src/driver/environment.rs

+    /// creating one Emerald and Reth instance per [crate::NODES].
+    pub fn init(&mut self) -> Result<()> {
+        // Reset the driver
+        *self = Default::default();


can you explain this line ?

I would rather prefer pub fn reinit(self) -> Result<Self> { ... }

rnbguy · 2026-02-05T17:55:13Z

tests/mbt/src/driver/environment.rs

+    /// - [FailureMode::ProcessRestart]: Restarts Emerald only
+    pub fn failure(&mut self, node: Node, mode: FailureMode) -> Result<()> {
+        if let FailureMode::ConsensusTimeout = mode {
+            // Noop wrt. MBT. The model will follow up with the propoer


Suggested change

// Noop wrt. MBT. The model will follow up with the propoer

// Noop wrt. MBT. The model will follow up with the proper

rnbguy · 2026-02-05T17:56:25Z

tests/mbt/src/driver/utils.rs

+impl EmeraldDriver {
+    /// Locates the system under test and use the driver's runtime to wait for
+    /// the execution of the given future.
+    pub fn perform<'a, F, Fut>(&'a mut self, node: Node, action: F) -> Result<()>


curious why this is implemented separately.

rnbguy · 2026-02-05T18:11:24Z

tests/mbt/src/sut/receive_proposal.rs

+        let peer_id = PeerId::from_multihash(Default::default())
+            .map_err(|err| anyhow!("Failed to create peer id: {err:?}"))?;


so, it's always from the same peer_id?

rnbguy · 2026-02-05T18:13:18Z

tests/mbt/src/sut/get_decided.rs

+            })
+            .transpose()?;
+
+        if proposal != emerald_proposal {


you can use anyhow::ensure

rnbguy · 2026-02-05T18:26:13Z

tests/mbt/src/driver/utils.rs

+        F: FnOnce(&'a mut Sut, &'a mut History) -> Fut,
+        Fut: Future<Output = Result<()>>,


don't know if it'll fit nicely but there exists AsyncFnOnce.

rnbguy · 2026-02-05T18:27:36Z

.github/workflows/test.yml

+    runs-on: ubuntu-latest
+    # XXX: Do not block on MBT initially until we gain confidence CI is not
+    # flaky for any reason.
+    continue-on-error: true


can you also add a timeout here ?

erickpintor requested review from jmalicevic and mpoke January 29, 2026 13:26

erickpintor requested a review from a team as a code owner January 29, 2026 13:26

erickpintor force-pushed the erick/introduce-mbt-suite branch 4 times, most recently from 029e72f to d09bd51 Compare January 29, 2026 21:14

erickpintor changed the base branch from erick/fix-reth-recreate to erick/mbt-reset-timeouts January 29, 2026 21:14

erickpintor commented Jan 29, 2026

View reviewed changes

erickpintor requested a review from bugarela January 29, 2026 22:04

bugarela approved these changes Jan 30, 2026

View reviewed changes

erickpintor force-pushed the erick/mbt-reset-timeouts branch from 9b46ba5 to 6343e8e Compare February 3, 2026 14:25

erickpintor force-pushed the erick/introduce-mbt-suite branch 4 times, most recently from 58ca2f7 to 1de9af2 Compare February 3, 2026 15:23

erickpintor force-pushed the erick/mbt-reset-timeouts branch from 6343e8e to b9b7e32 Compare February 4, 2026 13:25

erickpintor force-pushed the erick/introduce-mbt-suite branch from 1de9af2 to 54fca10 Compare February 4, 2026 13:28

erickpintor force-pushed the erick/mbt-reset-timeouts branch from b9b7e32 to 133095a Compare February 4, 2026 13:30

Base automatically changed from erick/mbt-reset-timeouts to main February 4, 2026 13:45

erickpintor force-pushed the erick/introduce-mbt-suite branch 2 times, most recently from 9f61e97 to 3d62414 Compare February 4, 2026 14:18

test(mbt): Add Model Based Test for Emerald

805fcc9

This patch connects the newly added Quint specs to Emerald's code via the Quint Connect library.

erickpintor force-pushed the erick/introduce-mbt-suite branch from 3d62414 to 805fcc9 Compare February 4, 2026 16:56

Merge branch 'main' into erick/introduce-mbt-suite

2f24a10

rnbguy reviewed Feb 5, 2026

View reviewed changes

	// Noop wrt. MBT. The model will follow up with the propoer
	// Noop wrt. MBT. The model will follow up with the proper

		let peer_id = PeerId::from_multihash(Default::default())
		.map_err(\|err\| anyhow!("Failed to create peer id: {err:?}"))?;

		F: FnOnce(&'a mut Sut, &'a mut History) -> Fut,
		Fut: Future<Output = Result<()>>,

Conversation

erickpintor commented Jan 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

bugarela left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

erickpintor commented Jan 29, 2026 •

edited

Loading